Inference at * 1 1 
Iof proof for Lemma bool-to-neg-dcdr wf:

.....assertion..... NILNIL

1. A : Type
2. f : A
3. A
  {f}  (x:A. Dec(f(x) = ff)) 

latex

 by (Unfold `bool-to-neg-dcdr` 0) 
CollapseTHEN (Auto) 

latex

C.

Definitions	{f}, bool-to-neg-dcdr-aux, x:AB(x), Type, Dec(P), x:A. B(x), , s = t, , f(a), ff, t  T
Lemmas	bool-to-neg-dcdr-aux, decidable wf, bool wf, bfalse wf